Normal(A,I)
== Normal(A)
== & (i:Id.
== & ((i  ma-interface-locs(I))
== & ( (Normal(ma-interface-ds(I;i))
== & ( & (k:Knd. (k  ma-interface-dom(I;i))  Normal(ma-interface-valtype(I;i;k))))) 

latex

---

clarification:

ma-interface-normal{i:l}
ma-interface-normal(A; I)
== normal-type{i:l}
== normal-type(A)
== & (i:Id.
== & ((i  ma-interface-locs(I)  Id)
== & ( (normal-ds{i:l}
== & ( (normal-ds(ma-interface-ds(I;i))
== & ( & (k:Knd.
== & ( & ((k  ma-interface-dom(I;i)  Knd)
== & ( & ( normal-type{i:l}
== & ( & ( normal-type(ma-interface-valtype(I;i;k))))) 

latex

Definitions	ma-interface-locs(I), Id, P & Q, Normal(ds), ma-interface-ds(I;i), x:A. B(x), P  Q, (x  l), ma-interface-dom(I;i), Knd, Normal(T), ma-interface-valtype(I;i;k)
FDL editor aliases	ma-interface-normal